package simplytyped

object SimplyTypedTests {
  import SimplyTypedLambda._
  import TypedLambdaParser.parseString
  import NameContext.desugar
  
  def testIdBool {
    val idBoolAST = L("x",TyBool, V(0))
    val code = "\\x:bool.x"
    val idparsed = parseString(code) getOrElse( exit)
    val (ctx,idparsconv) = desugar(idparsed)
    if (!(idBoolAST equals idparsconv)) 
      println("desugar doesn't work properly")
    if (!(
        idBoolAST.toString_(new Context[NameBinding](Nil))
        equals (idparsconv.toString_(new Context[NameBinding](Nil))) ))
      println("idBool and idparsconv differ")
      
    val idtype = LTerm.typeOf(idBoolAST)
    if (!(idtype equals TyArr(TyBool, TyBool))){
     ////println("OK: id is TyBool -> TyBool : "+idtype)} else
      println("id is not TyBool: "+idtype)}
    val idapplied = A(idBoolAST,Tru)
    if (!(LTerm typeOf idapplied equals TyBool)) 
      println("ERROR: type of id bool is wrong")
    val idappliedwrong = A(idBoolAST, V(0))
    try {LTerm typeOf idappliedwrong}
    catch {
      case e: TypeExc => () //println("OK: detected typing error")
    }
    if (!(LTerm.eval(idapplied) equals Tru))
      println("ERROR: eval not working for id bool") 
    eval(code)
    
  }
  
  def testIdInt {
    val idIntAST = L("x",TyInt, V(0))
    val code = "\\x:int.x"
    val idparsed = parseString(code) getOrElse( exit)
    val (ctx,idparsconv) = desugar(idparsed)
    if (!(idIntAST equals idparsconv)) println("desugar doesn't work properly")
    if (!(
        idIntAST.toString_(new Context[NameBinding](Nil))
        equals (idparsconv.toString_(new Context[NameBinding](Nil))) ))
      println("id and idparsconv differ")
      
    val idtype = LTerm typeOf idIntAST
    if (! (idtype equals TyArr(TyInt, TyInt)))
      println("id is not TyInt: "+idtype)
    val idapplied = A(idIntAST,Lit(4))
    if (!(LTerm typeOf idapplied equals TyInt))
      println("ERROR: type of id 4 is wrong")
    val idappliedwrong = A(idIntAST, Tru)
    try {LTerm typeOf idappliedwrong}
    catch {
      case e: TypeExc => //println("OK: detected typing error")
    }
    if (!(LTerm.eval(idapplied) equals Lit(4)))
      println("ERROR: eval not working for id 4") 
    eval(code)
  }
  
  
  def testifthenelse {
    val ifthenAST = If(Fls(),Tru(),Fls()) 
    val code = "if false then true else false"
    val ifthenparsed = parseString(code) getOrElse exit
    if (!(
        ifthenAST.toString_(new Context[NameBinding](Nil))
        equals (ifthenparsed.toString_(new Context[NameBinding](Nil))) ))
      println("ifthen and ifthenparsed differ")
    eval(code)
      
  }
  def test01kwi {
    eval("let x = 23 in ( ((\\y:bool z:int . x) (true)) 2)")
  }
  def testEx9_2_2_1 {
    val ex9_2_2_1AST=A( L("x",TyBool,V(0)) , If(Fls(),Tru(),Fls())  )
    val code = "(\\x:bool.x) (if false then true else false)"
    val parsedAST = parseString(code) getOrElse exit
    val ex9_2_2_1_type = TyBool
    if (!(LTerm.typeOf(ex9_2_2_1AST) equals ex9_2_2_1_type))
      println("ERROR: error type in ex9_2_2_1")
   if (!(LTerm.eval(ex9_2_2_1AST) equals Fls()))  println("ERROR: error eval ex9_2_2_1")
   eval(code)
  }
  def testInvert {
    val code = "let not = (\\x:bool . (if true then false else true)) in ( (\\y: (bool => bool) . (y (true))) not)"
    eval(code)
  }
  
  // is variable capture handled properly?
  def testBinding {
    val code = "(\\f: (int => int) . \\x: bool. \\y: int. (f y)) (\\x: int . x) (true) (5)" // TODO: improve parser so redundant parens can be omitted 
    val parsedAST = parseString(code) getOrElse exit
    println(eval(code))
  }
  
  // test whether computation indeed loops... >:-)
  def testLoopy {
    println("testLoopy")
    val code = "(\\f:(bool => bool) . f f) (\\f:(bool => bool) . f f)" 
    println(eval(parse(code)))
  }

  def testChunkUnwrap {
    val code = "(\\_: unit . 3) (unit)"
    println(eval(code))
  }
 
def main(args: Array[String]) {

   testIdBool
   testIdInt
   testifthenelse
   test01kwi
   testEx9_2_2_1
   testInvert
   testBinding
   //testLoopy
   testChunkUnwrap
  }
}